Course Title: Intermediate Logic

[For second-year philosophy undergraduates and above, who are specially interested in formal logic, the philosophy of language and logic, the philosophy of science; Fall semester, (credits 3)]

This course is in essence an intermediate-level course for formal logic. I shall hence assume that the student has a nodding acquaintance with topics in Elementary Logic. Some basic knowledge of Elementary Set Theory is extremely helpful though not essential. I shall confine this course to the four main styles of formal systems for propositional logic (i.e.CPC) and predicate logic(i.e., CQC):

(a) Hilbert-Frege style (axiom) systems,
(b) Systems of natural deduction,
(c) (Formal) tableaux systems, and
(d) Sequent calculi.

The syllabus is to be described as below:

The construction of a formal language suitable for propositional logic, and the standard semantics Application of arguments by cases, and proofs by induction
Formal proofs of general properties of semantic entailments, and some important results in propositional logic, including functional completeness, expressive adequacy, disjunctive normal form (DNF) and conjunctive normal form (CNF), the interpolation theorem, compactness, and decidability
The construction of formal systems
Formal proofs of the soundness theorem and completeness theorem for propositional logic.
The construction of axiomatic systems, systems of natural deduction, formal tableaux systems, and sequent calculi for propositional logic
The construction of a first-order language suitable for predicate logic and the standard semantics
Substitutional interpretation of quantification and objectual interpretation of quantification: true-in-i-interpretation in a structure and i-equivalence interpretation; true-in-M (a structure) and true-in-M+ (an expansion of M); a Tarskian style semantics
The congruence theorem, prenex normal form (PNF) and compactness of first-order language, Skolemization: Skolem functions, Skolemized form and Skolem axioms
The construction of axiomatic systems for predicate logic, the independence of axioms and the nature of axioms.
The construction of systems of natural deduction for predicate logic, and normalization of natural deduction
The construction of systems of formal tableaux for predicate logic.
The construction of sequent calculi for predicate logic and its normalization
Formal proofs of the soundness and completeness theorem for predicate logic, the decidability/ undecidability of first-order languages
The equivalence of systems of distinct styles

Problem sheets will be distributed each week; the student is expected to spend about 5 hours per week doing the exercises. Answers will be marked and return in the class.


Contents

Part I Formalization of Propositional Logic (CPC)


Introduction

1 A formal language suitable for CPC and the standard (classical) semantics
_ A formal propositional language K: alphabet; connectives, formation rules
_ A propositional language based on Polish notations system
_ Some basic syntactic properties of K
_ Arguments by cases, proof by induction
_ The standard (classical) semantics for K: structures vs. Boolean functions, semantic sequents
_ Some general properties of semantic entailments
_ Substitution theorem and logical equivalence; congruence theorem; duality theorem

2 Some semantic metatheorems for propositional logic
_ Truth-functions, expressive adequacy of K and functional completeness theorem
_ DNF/CNF, the interpolation theorem
_ Compactness of K
_ Decidability of K

3 The construction of formal systems: A survey
_ Derivations, axioms and rules of inferences, structural rules
_ Two types of derivations: derivations set out linearly and diagrammatically, respectively
_ Syntactic sequents, consistency, theorems
_ General approach to a formal proof of the soundness theorem
_ General approach to a Henkin-style proof of the completeness theorem
_ G_del`s incompleteness theorems

4 Axiomatic systems for CPC
_ The characteristics of axiom systems
_ An axiom system HPC for CPC
_ The deduction theorem
_ The soundness theorem for HPC
_ The completeness theorem for HPC: Post`s proof, Kalmar`s proof and Henkin`s proof
_ The independence of axioms, some remarks on the nature of axioms

5 Systems of natural deduction for CPC
_ The motivation for the establishment of natural deduction systems
_ The characteristics of natural deduction systems - introduction rules and elimination rules
_ Some formal systems of natural deduction
_ The equivalence of axiomatic systems and systems of natural deduction
_ Local-completeness of rules of inference for connectives
_ A special system of natural deduction N for CPC

6 Formal tableaux systems for CPC
_ Tableaux and formal tableaux systems
_ A tableaux system T for CPC, the soundness theorem and completeness theorem
_ The search of counterexamples in non-closed tableaux
_ Structural rules in tableaux systems
_ A more concise tableaux system
_ Tableaux system with signed formulae
_ A tableau proof of interpolation theorem and DNF theorem.

7 Sequent calculi for CPC
_ Gentzen`s sequents and sequent calculi
_ Axiomatization of entailment relations
_ Gentzen`s calculi and the construction of derivations
_ A sequent calculus with rules corresponding to tableau rules
_ Local-completeness of rules of inference for connectives in GS
_ Equivalence of sequent calculi and tableau systems

Part II Formalization of Predicate Logic (CQC)

8 A first-order language with identity suitable for CQC and the intended semantics
_ Elements of first-order language
_ A na_ve first-order language Q suitable for CQC
_ Preliminary to classical semantics for Q
_ Substitutional interpretation of quantification: structures and semantic rules for Q
_ Objectual interpretation of quantification: structures and semantic rules for Q
_ I-structure based semantics for Q: true-in-i-interpretation in a structure and i-equivalence
_ E-structure based semantics for Q: true-in-M (a structure) and true-in-M+ (an expansion of M)
_ Semantic entailment, validity and inconsistency

9 A Tarskian semantics and some general semantic properties of predicate logic
_ A more useful first-order language C with identity for predicate logic
_ A Tarskian semantics for C
_ Some semantic theorems concerning identity; the congruence theorem for C
_ Some semantic theorems concerning universal quantifier
_ Prenex normal form (PNF)
_ Decidability of first-order language
_ General properties of adequate formal systems for predicate logic and counterexample
_ Skolemization: Skolem functions, Skolemized form and Skolem axioms

10 Axiom systems for CQC
_ Axioms for quantified formulae
_ Rules of inference for quantified formulae
_ Axioms for identity in quantified formulae
_ An axiomatic system for predicate logic HQ
_ A Henkin-style proof of the completeness theorem for HQ
_ Independence of the axioms for quantified formulae in HQ

11 Natural deduction systems for CQC
_ A system of natural deduction for predicate logic NQ
_ Rules for quantifiers in natural deduction systems which accept open formulae as theorems
_ Soundness theorem and completeness theorem
_ Equivalence between axiom systems and systems of natural deduction
_ Normalization of natural deductions

12 Tableaux systems for CQC
_ Tableau rules for quantifiers and identity
_ Counterexamples
_ A tableau proof of the soundness theorem
_ A tableau proof of the completeness theorem
_ Tableaux systems with signed formulae for predicate logic

13 Sequent calculi for CQC
_ A sequent calculus for predicate logic with rules corresponding to a natural deduction system
_ A sequent calculus for predicate logic with rules corresponding to a tableaux system
_ Gentzen`s cut-free sequent calculus for predicate logic
_ The elimination of Cut Theorem and the normalization of sequent calculus

14 Beyond predicate logic
_ Pure logic vs. applied logic
_ A first-order number theory
_ Second-order logic
_ Many-sorted first-order logic
_ -logic and infinitary logic
_ Weak second-order logic

15 Free logic and inclusive logic

Suggested Textbooks

For overall:

J. Barwise (ed.), Handbook of Mathematical Logic, Amsterdam: North-Holland, 1977.
D. Bostock, Intermediate Logic, Oxford: Clarendon Press, 1997.
D. Scott, et. al., Notes on the Formalization of Logic, Sub-faculty of Philosophy, Oxford University, 1981.
G_ran Sundholm, `Systems of Deduction` (Chapter 1.2 of Handbook of Philosophical Logic).

For axiom systems:

A.G.Hamilton, Logic for Mathematicians, Cambridge: Cambridge Unuversuty Press, 1988, Chapters 1-4 and sections 1, 2 of Chapter 5.

For systems of natural deduction with the derivations set out linearly:

E. J. Lemmon, Beginning Logic, Chapman and Hall, 1965.

For systems of natural deduction with the derivations set out diagrammatically:

D. van Dalen, Logic and Structure, 3rd edition, Springer-Verlag, New York, 1994.
N. W. Tennant, Natural Logic, Edinburgh University Press, 1978.

For systems of formal tableaux:

R. C. Jeffrey, Formal Logic: Its scope and limits, 3rd ed., McGraw-Hill, Inc., 1991.
R. M. Smullyan, First-order Logic, New York: Dover Publication, Inc., 1995; original edition by Springer-Verlag, New York, 1968.

For sequent calculi:

There is no particular logic textbook adopting this system; but one can find some version of this type in some introductory books to other branches of formal logic, e.g. G. Takeuti, Proof Theory, (2nd ed., North Holland), 1987, Chapter One.